m, n, k:, f:(nm), g:(km).
increasing(f;n)
 increasing(g;k)
 (i:m. (j:n. i = f(j)  )  (j:k. i = g(j)  ))
 (j1:n, j2:k. f(j1) = g(j2)  )
 m = n+k   

latex

Definitions	AB, False, P  Q, A, Prop, P  Q, x:A. B(x), increasing(f;k), S  T, S  T, {i..j}, x:A. B(x), t  T, , Inj(A; B; f), 1of(t), i  j < k, P & Q, T, True, SQType(T), {T}, if b t else f fi, i<j, Unit, P  Q, P  Q, , ij, b, b
Lemmas	increasing inj, bnot wf, assert wf, le wf, le int wf, bool wf, lt int wf, assert of le int, bnot of lt int, true wf, squash wf, eqff to assert, iff transitivity, assert of lt int, eqtt to assert, inject wf, injection le, nat wf, int seg wf, increasing wf, not wf